// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_MATH_VECTOR_H
#define _sHT_MATH_VECTOR_H

/* TODO: prove many lemma's, probably with ghost functions
   (perhaps not implemented in Frama-C, see VCC papers) or in Coq. */

/*@ // Some common operations on vectors

    axiomatic VectorMinmax {
      predicate vector_lt_constant(\list<ℤ> v, ℤ k) = ∀ ℤ j;
        0 <= j < \length(v) ==> \nth(v, j) < k;
      predicate vector_le_constant(\list<ℤ> v, ℤ k) = ∀ ℤ j;
        0 <= j < \length(v) ==> \nth(v, j) <= k;

      lemma vector_lt_constant_split: ∀ \list<ℤ> v, u, ℤ k;
        vector_lt_constant(v, k) && vector_lt_constant(u, k)
        <==> vector_lt_constant(v ^ u, k);
      lemma vector_lt_constant_peelr: ∀ \list<ℤ> v, ℤ d, k;
        vector_lt_constant(v, k) && d < k
        <==> vector_lt_constant(v ^ [| d |], k);

      predicate vector_gt_constant(\list<ℤ> v, ℤ k) = ∀ ℤ j;
        0 <= j < \length(v) ==> \nth(v, j) > k;
      predicate vector_ge_constant(\list<ℤ> v, ℤ k) = ∀ ℤ j;
        0 <= j < \length(v) ==> \nth(v, j) >= k;
    }

    // Actually only +, not -, for the moment
    axiomatic VectorSign {
      predicate vector_eq0(\list<ℤ> v) = ∀ ℤ j;
        0 <= j < \length(v) ==> \nth(v, j) == 0;
      predicate vector_gt0(\list<ℤ> v) = ∀ ℤ j;
        0 <= j < \length(v) ==> \nth(v, j) > 0;
      predicate vector_ge0(\list<ℤ> v) = ∀ ℤ j;
        0 <= j < \length(v) ==> \nth(v, j) >= 0;

      lemma vector_gt0_gt_constant: ∀ \list<ℤ> v;
        vector_gt0(v) <==> vector_gt_constant(v, 0);
      lemma vector_ge0_ge_constant: ∀ \list<ℤ> v;
        vector_ge0(v) <==> vector_ge_constant(v, 0);
    }

    axiomatic VectorSum {
      logic ℤ sum(\list<ℤ> v);

      axiom sum_empty: sum([| |]) == 0;
      axiom sum_one: ∀ ℤ x; sum([| x |]) == x;
      axiom sum_split: ∀ \list<ℤ> v, u; sum(v ^ u) == sum(v) + sum(u);

      lemma sum_approximate_le: ∀ \list<ℤ> v, ℤ k;
        vector_le_constant(v, k) ==> sum(v) <= \length(v) * k;
      lemma sum_approximate_ge: ∀ \list<ℤ> v, ℤ k;
        vector_ge_constant(v, k) ==> sum(v) >= \length(v) * k;
    }

    // multiply all elements
    axiomatic VectorProduct {
      logic ℤ product(\list<ℤ> v);

      axiom product_empty: product([| |]) == 1;
      axiom product_one: ∀ ℤ x; product([| x |]) == x;
      axiom product_split: ∀ \list<ℤ> v, u; product(v ^ u) == product(v) * product(u);

      // More approximation lemma's in <sHT/math/expnat.h>
      lemma product_approximate_ge0: ∀ \list<ℤ> v;
        vector_ge0(v) ==> product(v) >= 0;
      lemma product_approximate_gt0: ∀ \list<ℤ> v;
        vector_gt0(v) ==> product(v) > 0;
    }

    // multiply element-wise
    axiomatic VectorCross {
      logic \list<ℤ> cross(\list<ℤ> v, \list<ℤ> u);

      axiom cross_length: ∀ ℤ i, \list<ℤ> v, u;
        \length(v) == \length(u) ==> \length(cross(v, u)) == \length(v);
      axiom cross_element: ∀ ℤ i, \list<ℤ> v, u;
        0 <= i < \length(v) == \length(u) ==>
        \nth(cross(v, u), i) == \nth(v, i) * \nth(u, i);

      lemma cross_empty: cross([| |], [|  |]) == [| |];
      lemma cross_one: ∀ ℤ x, y; cross([| x |], [| y |]) == [| x * y |];
      lemma cross_split: ∀ \list<ℤ> u0, u1, v0, v1;
        \length(u0) == \length(v0) && \length(u1) == \length(v1) ==>
        cross(u0 ^ u1, v0 ^ v1) == \concat(cross(u0, v0), cross(u1, v1));
    } */

#endif
